Step of Proof: bool-decider_wf
11,40
postcript
pdf
Inference at
*
I
of proof for Lemma
bool-decider
wf
:
b
:
. bool-decider(
b
)
Dec(
b
)
latex
by ((Unfold `bool-decider` 0)
CollapseTHEN (Auto
))
latex
Co
.
Definitions
bool-decider(
b
)
,
x
:
A
.
B
(
x
)
,
origin
b:
. bool-decider(b) 
Dec(
b)
by ((Unfold `bool-decider` 0)
))
b:. bool-decider(b) Dec(b)
by ((Unfold `bool-decider` 0)
))
x:A. B(x)